Nuprl Lemma : subtype-fpf2
0,22
postcript
pdf
A
:Type,
B1
,
B2
:(
A
Type). (
a
:
A
.
B1
(
a
)
B2
(
a
))
a
:
A
fp
B1
(
a
)
a
:
A
fp
B2
(
a
)
latex
Definitions
P
Q
,
x
.
t
(
x
)
,
a
:
A
fp
B
(
a
)
,
S
T
,
S
T
,
(
x
l
)
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
l
member
wf
,
fpf
wf
origin
A:Type, B1, B2:(A
Type). (a:A. B1(a) 
B2(a)) 
a:A fp B1(a) a:A fp B2(a) A:Type, B1, B2:(AType). (a:A. B1(a) B2(a)) a:A fp B1(a) a:A fp B2(a) Q
x. t(x) B(a)
T T
l)x:A. B(x) T